nLab smooth homotopy type

Idea

In view of the congruence of the notions of homotopy type and type in homotopy type theory it makes sense to refer to an object in a cohesive (∞,1)-topos $\mathbf{H}$ such as as Smooth∞Grpd as a smooth homotopy type or smooth infinity-groupoid. Accordingly then an n-truncated object in $\mathbf{H}$ is a smooth $n$-type.

For instance a smooth 0-type is then an object in the sheaf topos $Sh(CartSp) \hookrightarrow Sh_\infty(CartSp) \simeq \mathbf{H}$ of smooth sets.

Related concepts

• smooth homotopy

References

• geometry of physics – smooth homotopy types